I want to kind of tell you a little bit about complexity essentially.

I've been reminding you very often that this problem is NP-hard,

which means it's hard and exponential in the worst case.

That's all we know.

We know in this huge sea of formulae we could come up with, some of them are really, really, really hard to solve.

Now, it makes a difference whether almost all of them are really, really, really hard to solve,

or there's only one that is really, really hard to solve.

Huge numbers are actually really, really easy.

This is a question that worst-case complexity cannot answer.

It's an interesting question, and we don't really have a good mathematical model we do.

It's called statistics, and it's awfully hard to actually do in practice,

because the things you're interested in you cannot really measure most of the time.

The good thing is that since solving SAT problem is so important, people have actually found ways of measuring.

Here it's really, really simple actually.

When you start measuring how long your SAT solver runs,

and you come up with the idea of making that parametric,

and taking as the parameter the ratio between claw length and number of variables.

If you have many variables, you have a lot of choice for interpretations.

If you have lots of variables in small clauses, then you have many ways of making the clauses true,

so it should be relatively easy.

Many variables in short clauses should essentially all become satisfiable,

whereas long clauses with few variables should all become unsatisfiable.

I think of clauses as constraints, and if you have lots of constraints, it's probably over-constrained.

That's something we see in practice as well, and you would naively think,

well, you start out with 100 percent, if you have this kind of relation as a parameter,

100 percent satisfiable going down to 100 percent unsatisfiable.

We see what you think of as a phase transition.

You basically have for a long time, everything is satisfiable,

and for a long time here, everything is unsatisfiable.

Depending on various factors, this threshold is even much stronger.

That's something we empirically see.

The bigger the numbers all in all get, the sharper this cliff gets.

The other thing we see, if we measure runtimes,

we see that the runtimes in these cases where it's supposedly clear is very short,

and then we see a peak that very well coincides with the point of the phase transition.

We know where the hard problems are.

We can measure and predict which problems are going to be hard.

Those here at 4.3 or something like this, which is an empirical constant for clauses NTPLL and so on,

which is nice if you're designing competitions.

It tells you exactly what to do.

Randomly generate a clause set that has a ratio of 4.3.

Feed it to the people, watch them tear out their hair.

That's something we can kind of explain by these ideas of under and over constraint,

and that we see in lots of NP-hard problems.

The good thing here is that if you compare this area to that area,

which is kind of how good is my worst-case estimate,

the worst-caseness of this is quite bad,

which means unless you're unlucky and get some problem here,

computation is going to be quick because it has a lot of structure,

because it is under-constrained and gives you freedom and so on, these kind of things.